from cheqed.core.sexp import sexp, sexp_to_string

class Term:
    def __str__(self):
        return sexp_to_string(self.sexp())

    def __repr__(self):
        return str(self)

class Variable(Term):
    def __init__(self, name):
        self.name = name

    def sexp(self):
        return self.name

    def __eq__(self, other):
        return isinstance(other, Variable) \
               and self.name == other.name

    def __hash__(self):
        return hash(self.name)

    def substitute(self, a, b):
        if self == b:
            return a

        return self

    def free_variables(self):
        return set([ self ])

class Function(Term):
    def __init__(self, name, *args):
        self.name = name
        self.args = args

    def sexp(self):
        return [self.name] + [sexp(term) for term in self.args]

    def __eq__(self, other):
        return isinstance(other, Function) \
               and self.name == other.name \
               and self.args == other.args

    def substitute(self, a, b):
        if self == b:
            return a

        return Function(self.name,
                        *[term.substitute(a, b) for term in self.args])
    
    def free_variables(self):
        return reduce(lambda x, y: x.union(y),
                      [term.free_variables() for term in self.args],
                      set())

class Separation(Term):
    name = 'separation'
    operator = name

    def __init__(self, variable, domain, formula):
        assert variable not in domain.free_variables()
        
        self.variable = variable
        self.domain = domain
        self.formula = formula

    def sexp(self):
        return ([self.name,
                 sexp(self.variable),
                 sexp(self.domain),
                 sexp(self.formula)])

    def __eq__(self, other):
        return (self.__class__ == other.__class__
                and self.name == other.name
                and self.variable == other.variable
                and self.domain == other.domain
                and self.formula == other.formula)
    
    def substitute(self, a, b):
        if self == b:
            return a

        if b.free_variables().issubset(self.free_variables()):
            if self.variable in a.free_variables():
                raise SubstitutionError()

            return self.__class__(self.variable,
                                  self.domain.substitute(a, b),
                                  self.formula.substitute(a, b))
        
        return self
    
    def free_variables(self):
        return reduce(lambda x, y: x | y,
                      ((self.domain.free_variables()
                        | self.formula.free_variables())
                       - set(self.variable)),
                      set())
